R:Realizer, i:Id. R-Feasible(R)  R-da(R;i) = 1of(2of([[R]](i)))  k:Knd fp Type 

latex

Definitions

x:A. B(x), P  Q, R-da(R;i), 1of(t), 2of(t), [[R]], Prop, x. t(x), t  T, if b t else f fi, , @i: x:T initially x = v, @i: only L affects x : t, @i: only L sends on (l with tg), @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, @i: with declarations ds:dsda:da k(v) sends f s v on link l, @i (with ds: ds action a:T precondition a(v) is P s v), @i: k affects only members of L, @i: k sends only links in L, @i: only members of L read x, , mk-ma, x : t initially x = v, true, false, only members of L affect x :t, only L sends on (l with tg), with declarations ds:dsda:daeffect of k(v) is x := f s v, with declarations ds:dsda:dak(v) sends f s v on link l, (with ds: ds action a:T precondition a(v) is P s v), k affects only members of L, k sends only on links in L, only members of L read x, A  B, M1  M2, T, True, x(s), {T}, MsgA, , Unit, P  Q, P & Q, A, False, R-Feasible(R), Dsys, a = b,

Lemmas

es realizer-induction, Id wf, R-Feasible wf, fpf wf, Knd wf, R-da wf, R-Dsys wf, msga wf, pi1 wf, fpf-cap wf, id-deq wf, ma-state wf, ma-valtype wf, locl wf, pi2 wf, IdLnk wf, Kind-deq wf, rcv wf, top wf, es realizer wf, fpf-empty wf, Rnone wf, eq id wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert-eq-id, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, Rinit wf, Rframe wf, lsrc wf, Rsframe wf, fpf-single wf, Reffect wf, decl-state wf, decl-type wf, fpf-join wf, lnk-decl wf, Rsends wf, Rpre wf, Raframe wf, Rbframe wf, Rrframe wf, squash wf, true wf, deq wf